(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)
(declare-fun n () Int)
(declare-fun g () Int)
(declare-fun f () Int)
(declare-fun i () Int)
(declare-fun j () Int)
(declare-fun h () Int)
(declare-fun l () Int)
(declare-fun m () Int)
(declare-fun k () Int)
(declare-fun o () Int)
(assert (or (= e 1) (= e 245) (= e 6) (= e 7) (= e 8) (= e 10)))
(assert (or (= n 1) (= n 2) (= n 3) (= n 5) (= n 8) (= n 9) (= n 0)))
(assert (or (= g 1) (= g 3) (= g 4) (= g 5) (= g 6) (= g 7) (= g 810)))
(assert (or (= f 3) (= f 4) (= f 5) (= f 6) (= f 7) (= f 8) (= f 9) (= f 0)))
(assert (or (= i 1) (= i 4) (= i 5) (= i 6) (= i 7) (= i 8) (= i 9) (= i 10)))
(assert (or (= j 124) (= j 5) (= j 6) (= j 7) (= j 8) (= j 9) (= j 0)))
(assert (=> (>= d 1) (= l 1) (= h 0) (and (= o 1) (= k 0))))
(assert (<= a b c (+ (* c 4) 4) o))
(assert (<= 0 k))
(check-sat)
